/* This file is used by the HTML files that make-html.py creates. 
   Customize this if you want to create HTML files with different
   colors. See also make-html.py's --pygments-style option. */
body {
    color: white;
    background-color: #222222;
}
a {
    color: orange;
}
